package ch.epfl.lara.matcheck.tester;

import ch.epfl.lara.matcheck.ast.parser.{MatcheckParser,SyntaxAnalyzer,FormulaParser, SyntaxParser}
import ch.epfl.lara.matcheck.ast._

trait TesterSkeleton {
  
  object ParsePhase extends MatcheckParser { self: MatcheckParser =>
    def apply(filename: String): Tree = try {
      if(fileExists(filename)) {
        Report.verbose("Analysing source: "+filename+"\n")
        test(parseFile(filename))
      } else {
        Report.cleanFail("File "+filename+" doesn't exists!\n")
        null
      }
    } catch {
      case e @ _ =>
        error(e.getMessage)
    }
    
    
    import java.io.File
    private def fileExists(filename: String): Boolean = new File(filename).isFile
    
    private def test(term: ParseResult[Tree]): Tree = {
      term match {
        case Success(term, _) => term
        case Failure(msg, remainder) =>
          error("Failure: "+msg+"\n"+"Remainder: \n"+remainder.pos.longString)
        case Error(msg, remainder) => 
          error("Error: "+msg+"\n"+"Remainder: \n"+remainder.pos.longString)
      }
    }
  }
  
  
  object FreshTreePhase { 
    import ch.epfl.lara.matcheck.util.FreshTree
    def apply(tree: Tree): Tree = FreshTree(tree)
  }
  

  object NameAnalyzePhase extends SyntaxAnalyzer {
    def apply(tree: Tree): Unit = tree match {
      case p: Program => analyzeProgram(p)
      case _ => Report.fail("NameAnalyzer must be called only with Program node")
    }
  }
  
  
  object DesugarPhase {
    import ch.epfl.lara.matcheck.ast.parser.Desugar
    def apply(tree: Tree): Tree = Desugar(tree)
  }
  
  
  object VerifyPhase {
    import ch.epfl.lara.matcheck.verify.{Verify,AxiomsHolder}
    def apply(tree: Tree): Unit = tree match {
      case p : Program =>
        AxiomsHolder(p)
        new Verify(p)
      case _ => 
        Report.fail("Verify must be called only with Program node")
    }
  }
 
}
